package bcontractor.propositional.factories;

import java.util.HashSet;
import java.util.Random;
import java.util.Set;

import bcontractor.propositional.PropositionalSentence;

/**
 * Factory for Horn clauses
 * 
 * @author lundberg
 * 
 */
public class HornClauseFactory implements SentenceFactory<PropositionalSentence> {

	private Random random;

	private int nVariables;

	private int minSize;

	private int maxSize;

	/**
	 * Constructor
	 * 
	 * @param random random
	 */
	public HornClauseFactory(Random random, int nVariables, int minSize, int maxSize) {
		if (maxSize > nVariables) {
			throw new IllegalArgumentException("maxSize should be less or equal to nVariables.");
		}
		if (minSize > maxSize) {
			throw new IllegalArgumentException("minSize should be less or equal to maxSize.");
		}
		this.random = random;
		this.nVariables = nVariables;
		this.minSize = minSize;
		this.maxSize = maxSize;
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public PropositionalSentence create(Integer... forcedAtoms) {
		if (forcedAtoms.length > maxSize) {
			throw new IllegalArgumentException("Forced atoms number exceeds maximum clause size.");
		}
		int minimal = Math.max(this.minSize, forcedAtoms.length);
		int clauseSize = minimal + random.nextInt(maxSize - minimal + 1);
		Set<Integer> atoms = new HashSet<Integer>();
		for (Integer forcedAtom : forcedAtoms) {
			atoms.add(Math.abs(forcedAtom));
		}
		while (atoms.size() < clauseSize) {
			Integer atom = random.nextInt(nVariables) + 1;
			atoms.add(atom);
		}
		int[] clause = new int[clauseSize];
		int index = 0;
		for (Integer atom : atoms) {
			clause[index++] = -atom;
		}
		if (random.nextBoolean()) {
			int randomIndex = random.nextInt(clause.length);
			clause[randomIndex] = -clause[randomIndex];
		}
		return new PropositionalSentence(clause);
	}
}
